app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(sum, app2(app2(cons, x), xs)) -> app2(app2(plus, x), app2(sum, xs))
app2(size, app2(app2(node, x), xs)) -> app2(s, app2(sum, app2(app2(map, size), xs)))
app2(app2(plus, 0), x) -> 0
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
↳ QTRS
↳ Non-Overlap Check
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(sum, app2(app2(cons, x), xs)) -> app2(app2(plus, x), app2(sum, xs))
app2(size, app2(app2(node, x), xs)) -> app2(s, app2(sum, app2(app2(map, size), xs)))
app2(app2(plus, 0), x) -> 0
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(sum, app2(app2(cons, x), xs)) -> app2(app2(plus, x), app2(sum, xs))
app2(size, app2(app2(node, x), xs)) -> app2(s, app2(sum, app2(app2(map, size), xs)))
app2(app2(plus, 0), x) -> 0
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(sum, app2(app2(cons, x0), x1))
app2(size, app2(app2(node, x0), x1))
app2(app2(plus, 0), x0)
app2(app2(plus, app2(s, x0)), x1)
APP2(app2(plus, app2(s, x)), y) -> APP2(s, app2(app2(plus, x), y))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
APP2(size, app2(app2(node, x), xs)) -> APP2(app2(map, size), xs)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
APP2(sum, app2(app2(cons, x), xs)) -> APP2(plus, x)
APP2(size, app2(app2(node, x), xs)) -> APP2(map, size)
APP2(sum, app2(app2(cons, x), xs)) -> APP2(app2(plus, x), app2(sum, xs))
APP2(size, app2(app2(node, x), xs)) -> APP2(s, app2(sum, app2(app2(map, size), xs)))
APP2(size, app2(app2(node, x), xs)) -> APP2(sum, app2(app2(map, size), xs))
APP2(app2(plus, app2(s, x)), y) -> APP2(app2(plus, x), y)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(sum, app2(app2(cons, x), xs)) -> APP2(sum, xs)
APP2(app2(plus, app2(s, x)), y) -> APP2(plus, x)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(cons, app2(f, x))
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(sum, app2(app2(cons, x), xs)) -> app2(app2(plus, x), app2(sum, xs))
app2(size, app2(app2(node, x), xs)) -> app2(s, app2(sum, app2(app2(map, size), xs)))
app2(app2(plus, 0), x) -> 0
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(sum, app2(app2(cons, x0), x1))
app2(size, app2(app2(node, x0), x1))
app2(app2(plus, 0), x0)
app2(app2(plus, app2(s, x0)), x1)
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
APP2(app2(plus, app2(s, x)), y) -> APP2(s, app2(app2(plus, x), y))
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
APP2(size, app2(app2(node, x), xs)) -> APP2(app2(map, size), xs)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
APP2(sum, app2(app2(cons, x), xs)) -> APP2(plus, x)
APP2(size, app2(app2(node, x), xs)) -> APP2(map, size)
APP2(sum, app2(app2(cons, x), xs)) -> APP2(app2(plus, x), app2(sum, xs))
APP2(size, app2(app2(node, x), xs)) -> APP2(s, app2(sum, app2(app2(map, size), xs)))
APP2(size, app2(app2(node, x), xs)) -> APP2(sum, app2(app2(map, size), xs))
APP2(app2(plus, app2(s, x)), y) -> APP2(app2(plus, x), y)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(sum, app2(app2(cons, x), xs)) -> APP2(sum, xs)
APP2(app2(plus, app2(s, x)), y) -> APP2(plus, x)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(cons, app2(f, x))
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(sum, app2(app2(cons, x), xs)) -> app2(app2(plus, x), app2(sum, xs))
app2(size, app2(app2(node, x), xs)) -> app2(s, app2(sum, app2(app2(map, size), xs)))
app2(app2(plus, 0), x) -> 0
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(sum, app2(app2(cons, x0), x1))
app2(size, app2(app2(node, x0), x1))
app2(app2(plus, 0), x0)
app2(app2(plus, app2(s, x0)), x1)
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
APP2(app2(plus, app2(s, x)), y) -> APP2(app2(plus, x), y)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(sum, app2(app2(cons, x), xs)) -> app2(app2(plus, x), app2(sum, xs))
app2(size, app2(app2(node, x), xs)) -> app2(s, app2(sum, app2(app2(map, size), xs)))
app2(app2(plus, 0), x) -> 0
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(sum, app2(app2(cons, x0), x1))
app2(size, app2(app2(node, x0), x1))
app2(app2(plus, 0), x0)
app2(app2(plus, app2(s, x0)), x1)
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
APP2(app2(plus, app2(s, x)), y) -> APP2(app2(plus, x), y)
APP1 > app2
plus > app2
s > app2
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(sum, app2(app2(cons, x), xs)) -> app2(app2(plus, x), app2(sum, xs))
app2(size, app2(app2(node, x), xs)) -> app2(s, app2(sum, app2(app2(map, size), xs)))
app2(app2(plus, 0), x) -> 0
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(sum, app2(app2(cons, x0), x1))
app2(size, app2(app2(node, x0), x1))
app2(app2(plus, 0), x0)
app2(app2(plus, app2(s, x0)), x1)
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
APP2(sum, app2(app2(cons, x), xs)) -> APP2(sum, xs)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(sum, app2(app2(cons, x), xs)) -> app2(app2(plus, x), app2(sum, xs))
app2(size, app2(app2(node, x), xs)) -> app2(s, app2(sum, app2(app2(map, size), xs)))
app2(app2(plus, 0), x) -> 0
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(sum, app2(app2(cons, x0), x1))
app2(size, app2(app2(node, x0), x1))
app2(app2(plus, 0), x0)
app2(app2(plus, app2(s, x0)), x1)
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
APP2(sum, app2(app2(cons, x), xs)) -> APP2(sum, xs)
app1 > APP1
cons > sum
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(sum, app2(app2(cons, x), xs)) -> app2(app2(plus, x), app2(sum, xs))
app2(size, app2(app2(node, x), xs)) -> app2(s, app2(sum, app2(app2(map, size), xs)))
app2(app2(plus, 0), x) -> 0
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(sum, app2(app2(cons, x0), x1))
app2(size, app2(app2(node, x0), x1))
app2(app2(plus, 0), x0)
app2(app2(plus, app2(s, x0)), x1)
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(size, app2(app2(node, x), xs)) -> APP2(app2(map, size), xs)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(sum, app2(app2(cons, x), xs)) -> app2(app2(plus, x), app2(sum, xs))
app2(size, app2(app2(node, x), xs)) -> app2(s, app2(sum, app2(app2(map, size), xs)))
app2(app2(plus, 0), x) -> 0
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(sum, app2(app2(cons, x0), x1))
app2(size, app2(app2(node, x0), x1))
app2(app2(plus, 0), x0)
app2(app2(plus, app2(s, x0)), x1)
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(f, x)
APP2(size, app2(app2(node, x), xs)) -> APP2(app2(map, size), xs)
APP2(app2(map, f), app2(app2(cons, x), xs)) -> APP2(app2(map, f), xs)
APP1 > app2 > map
cons > app2 > map
size > app2 > map
node > map
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
app2(app2(map, f), nil) -> nil
app2(app2(map, f), app2(app2(cons, x), xs)) -> app2(app2(cons, app2(f, x)), app2(app2(map, f), xs))
app2(sum, app2(app2(cons, x), xs)) -> app2(app2(plus, x), app2(sum, xs))
app2(size, app2(app2(node, x), xs)) -> app2(s, app2(sum, app2(app2(map, size), xs)))
app2(app2(plus, 0), x) -> 0
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
app2(app2(map, x0), nil)
app2(app2(map, x0), app2(app2(cons, x1), x2))
app2(sum, app2(app2(cons, x0), x1))
app2(size, app2(app2(node, x0), x1))
app2(app2(plus, 0), x0)
app2(app2(plus, app2(s, x0)), x1)